A:Type, eq:EqDecider(A), B:(AType), f, g:a:A fp B(a). f || f  g 

latex

Definitions	False, P  Q, A, x:A. B(x), b, t  T, b, s = t, , , x. t(x), f(a), x(s), f(x), x  dom(f), x:AB(x), x:A  B(x), P & Q, P  Q, Unit, left + right, Void, x:A.B(x), Top, a:A fp B(a), x.A(x), f  g, <a, b>, f || g, Type, EqDecider(T)
Lemmas	fpf wf, deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, bool wf, fpf-ap wf, bnot wf, not wf, assert wf